﻿using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using Microsoft.Pex.Framework;
using System.Collections;
using Microsoft.Pex.Framework.Goals;

namespace MicroBenchmarks.DataStructures
{
    /// <summary>
    /// Checks common datastructure arraylist
    /// </summary>
    [PexClass]
    [PexMe.Attribute.FieldAccessObserver]
    [PexMe.Attribute.InsufficientObjectFactoryObserver]
    public partial class ArrayListTest
    {
        [PexMethod]
        [PexAssertReachEventually]
        public void ArrayListSizeTest([PexAssumeUnderTest]ArrayListWrapper list)
        {
            if (list.Count > 1)
                PexAssert.ReachEventually();
        }

        [PexMethod]
        [PexAssertReachEventually]
        public void ArrayListContainsTest([PexAssumeUnderTest]ArrayListWrapper list)
        {
            if (list.Contains(100))
                PexAssert.ReachEventually();
        }

        //[PexMethod(MaxRunsWithoutNewTests = 20000, MaxConstraintSolverTime = 2)]
        //public void DiffGen(int[] ints1, int[] ints2)
        //{
        //    PexAssume.IsTrue(ints1 != null && ints1.Length == 9);
        //    PexAssume.AreDistinctValues(ints1);
        //    PexAssume.IsTrue(ints1[0] > 0 && ints1[0] < 10);

        //    PexAssume.IsTrue(ints2 != null && ints2.Length == 9);
        //    PexAssume.AreDistinctValues(ints2);
        //    PexAssume.IsTrue(ints2[0] > 0 && ints2[0] < 10);

        //    bool bAtleastone = false;
        //    for (int count = 0; count < ints1.Length; count++)
        //    {
        //        if (ints1[count] != ints2[count])
        //        {
        //            bAtleastone = true;
        //            break;
        //        }
        //    }

        //    PexAssume.IsTrue(bAtleastone);         


            
        //    PexAssert.IsTrue(MultiplyCheck1(ints1));
        //    PexAssert.IsTrue(MultiplyCheck1(ints2));
        //}


        //public bool MultiplyCheck1(int[] ints)
        //{
        //    PexAssume.IsTrue(ints != null && ints.Length == 9);
        //    PexAssume.AreDistinctValues(ints);
        //    PexAssume.IsTrue(ints[0] > 0 && ints[0] < 10);

        //    int result = 0, multiplicatinval = 2;

        //    bool begin = true;
        //    for (int count = 1; count < ints.Length; count++)
        //    {
        //        PexAssume.IsTrue(ints[count] > 0 && ints[count] < 10);

        //        if (begin)
        //        {
        //            result = ints[0] * 10 + ints[count];
        //            begin = false;
        //        }
        //        else
        //        {
        //            result = result * 10 + ints[count];
        //        }

        //        PexAssume.IsTrue(result % multiplicatinval == 0);
        //        multiplicatinval++;
        //    }

        //    return true;
        //}

        //[PexMethod]
        //public void MultiplyCheck2(int[] ints)
        //{
        //    PexAssume.IsTrue(ints != null && ints.Length == 9);
        //    PexAssume.AreDistinctValues(ints);
        //    PexAssume.IsTrue(ints[0] > 0 && ints[0] < 10);

        //    PexAssume.IsTrue(!(ints[0] == 3 &&
        //                       ints[1] == 8 &&
        //                       ints[2] == 1 &&
        //                       ints[3] == 6 &&
        //                       ints[4] == 5 &&
        //                       ints[5] == 4 &&
        //                       ints[6] == 7 &&
        //                       ints[7] == 2 &&
        //                       ints[8] == 9));
            

        //    int result = 0, multiplicatinval = 2;

        //    bool begin = true;
        //    for (int count = 1; count < ints.Length; count++)
        //    {
        //        PexAssume.IsTrue(ints[count] > 0 && ints[count] < 10);

        //        if (begin)
        //        {
        //            result = ints[0] * 10 + ints[count];
        //            begin = false;
        //        }
        //        else
        //        {
        //            result = result * 10 + ints[count];
        //        }

        //        PexAssume.IsTrue(result % multiplicatinval == 0);
        //        multiplicatinval++;
        //    }
        //}
    }
}
